#ifndef PDTGRAPHVISITOR_H
#define PDTGRAPHVISITOR_H
#include "PDTCodeGraph.h"
#include <vector>
#include <stack>
//#include "../../third/yices-1.0.27/include/yices_c.h"
extern "C"{
#include "yices_c.h"
#include"yicesl_c.h"
}
//added because of circular includes
class PDTNode;


class PDTGraphVisitor
{
public:    
	virtual bool pre(PDTNode * me)=0;
	virtual bool in(PDTNode * me, PDTNode* child,unsigned int i)=0;
	virtual bool post(PDTNode * me)=0;

};

class PDTDefaultVisitor:public PDTGraphVisitor{
public:
	virtual bool pre(PDTNode * me);
	virtual bool in(PDTNode * me, PDTNode* child, unsigned int i);
	virtual bool post(PDTNode * me);
	virtual ~PDTDefaultVisitor(){}
};




class PDTYicesVisitor:public PDTGraphVisitor{
public:
	stack<int> ifHelper;
	yices_context ctx;
	yicesl_context lctx;
	yices_type ty;
	string currentAssertion;
	int currentID;
	int previousID;
	void updateIDs(bool assertGreater);

	bool firstTime;
	bool assignTarget;
	bool ifCondition;
//	vector<string> prefixes;
//	vector<string> suffixes;
	void ECPrinter();
	void appendParan();
	virtual bool pre(PDTNode * me);
	virtual bool in(PDTNode * me, PDTNode* child,unsigned int i);
	virtual bool post(PDTNode * me);
	int declareNumVar(PDTNode * me);
	int declareBoolVar(PDTNode * me);
	char * stringToCharArray(string s);
	int writeToYices(string statement);
	int writeToYices(char* statement);
	int writeToYices(const char* statement);
	char * constCharToChar(const char * cArray);
	PDTYicesVisitor(PDTCodeGraph &CG);
	virtual ~PDTYicesVisitor(){}
};

#endif // PDTGRAPHVISITOR_H

